es:ES, C, V:Type, ASM:((C List)V), I:(E(?C)), O:(E(?V)),
R:({e:E| isl(O(e))} {e:E| isl(I(e))} ), H:({e:E| isl(I(e))} ({e:E| isl(I(e))}  List)).
dsm(es;ASM;I;O;R;V;H)   

latex

Definitions	S  T, P  Q, P  Q, P & Q, h-ordered(es;e.P(e);H), A c B, dsm(es;ASM;I;O;R;V;H), , t  T, x:A. B(x)
Lemmas	event system wf, unit wf, es-E wf, map wf3, outl wf, isl wf, iseg wf, es-causle wf, l member wf, assert wf